1. Technical Field
The present disclosure generally relates to verification techniques for integrated circuit logic design and in particular to techniques for constructing inductive counterexamples in a multi-algorithm verification framework.
2. Description of the Related Art
Formal verification techniques are powerful tools for the construction of correct logic designs. These verification techniques have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately, the techniques have the power to prove that the design is correct, i.e., that no failing scenario exists. Unfortunately, formal verification techniques require computational resources, and these computational resources are exponential with respect to the size of the design under test, requiring, in a worst case scenario, the analysis of every “reachable state” of a given design.
One approach that has demonstrated powerful potential to extend the capacity of automated formal verification techniques is the use of an interactive framework to control the dispatching of verification problems into an automated toolset, and to build upon results obtained from the toolset. For example, an expert human may interact with a theorem proving system to attempt to prove an extremely complex problem. In such paradigms, it is often the case that “induction” is used to solve the problem. And, in particular, inductive proofs seek to demonstrate that design states which do not violate properties within a given number of time-frames cannot violate properties within a larger number of time-frames. One major benefit of inductive techniques is that they do not rely upon expensive characterizations of reachable state sets, as often the property under verification may be demonstrated as correct from an arbitrary state which does not lead to a shallow failure of the property under verification. However, in general, inductive techniques are inconclusive since it may be the case that a property which does not fail requires a tighter characterization of the reachable states than is possible using induction reasoning alone. In particular, induction counterexamples often begin from “inductive starting states” which are in fact unreachable. In such a verification setting, it is critical to be able to present the user of the verification tool with a counterexample trace illustrating the scenario which fails an inductive check, as such feedback is critical to the user being able to augment his verification strategy.
Modern automated verification tools rely upon a large set of algorithms to enable efficient verification results. Particularly, they tend to rely upon reduction techniques which seek to reduce the size of the design under verification, to thereby yield exponential reductions to overall verification resources. For example, techniques such as “redundancy removal” may merge equivalent or constant gates and thereby reduce netlist size. There are many algorithmic frameworks wherein such redundant gates may be identified. The effectiveness of scalable light-weight proof techniques such as induction tends to be dramatically higher than that before such reduction, as the reductions themselves naturally rule out unreachable “inductive starting states” from the reduced netlist. “Lifting” inductive counterexamples, which constitute scenarios under which an inductive proof fails, is generally a challenging problem within a verification tool. First, such counterexamples do not originate from the designated initial states of a design; instead, they originate from an arbitrary inductive starting state. Second, in the presence of commonplace reduction techniques, care must be taken to ensure that the inductive starting state after such reductions may be mapped to one consistent with an inductive starting state before such reductions.